ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), a:ecl(ds; da), v:ecl-trans-tuple{i:l}(ds; da),
L:(event-info(ds;da) List).
(L:(event-info(ds;da) List). 
(ecl-trans-normal(v)  (n:. (ecl-trans-halt2(ds; da; v)(n,L))  (n  ecl-trans-es(v))))
 (n:. 
 (L':event-info(ds;da) List. (iseg(event-info(ds;da); L'; L)  (ecl-halt(ds; da; a)(n,L'))))
  (ecl-trans-halt2(ds; da; v)(n,L)))
 (m:. (ecl-act(ds; da; m; a)(L))  (ecl-trans-act(ds; da; v)(m,L))))
 (ecl-halt(ds; da; a)(0,L))
 (ecl-trans-state(reset-ecl-tuple(v); L)
 (=
 (ecl-trans-init(reset-ecl-tuple(v))
 ( ecl-trans-type(reset-ecl-tuple(v))) 

latex

Definitions

tt, Y, ff, t.1, if b then t else f fi , list_accum(x,a.f(x;a); y; l), spreadn(u; a,b,c,d,e,f,g.v(a;b;c;d;e;f;g)), ma-valtype(da; k), ecl-trans-state-from(v; z; L), ecl-trans-h(v), ecl-trans-init(v), reset-ecl-tuple(A), ecl-trans-type(A), A c B, P  Q, compat(T; l1; l2), ge(i; j), False, A, prop{i:l}, x. t(x), subtype(S; T), top, t  T, guard(T), A  B, x:A. B(x), , P  Q, P  Q, x:A. B(x), Unit, , event-info(ds;da), ecl-trans-tuple{i:l}(ds; da), P  Q, null(as), b, ||as||, decidable(P), P  Q, ecl-trans-halt2(ds; da; A), x(s),

Lemmas

not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, assert-deq-member, eqtt to assert, iff transitivity, bool wf, Kind-deq wf, deq-member wf, ecl-reset-state, ecl-trans-state-from wf, length-append, iseg length, member wf, iseg append0, iseg transitivity, ecl-halt-unique, ecl-trans-h wf, assert wf, ecl-trans-init wf, ecl-trans-state wf, ecl-trans-type wf, last wf, reset-ecl-tuple wf, ecl-trans-state-append, last lemma, ecl-halt-nil, null wf3, decidable assert, iseg weakening, ge wf, nat properties, ecl-trans-act wf, ecl-act wf, iseg wf, iff wf, ecl-trans-es wf, l member wf, nat plus inc, ecl-trans-halt2 wf, nat plus wf, ecl-trans-normal wf, le wf, ecl-halt wf, Id wf, Knd wf, fpf wf, ecl wf, ecl-trans-tuple wf, event-info wf, length wf1, top wf, length wf nat, nat wf